A:Type, eq:EqDecider(A), B:(AType), x,y:A, v:B(x), u:B(y).
((x = y)  (v = u  B(x)))
 fpf-compatible(A; a.B(a); eq; fpf-single(x; v); fpf-single(y; u)) 

latex

Definitions	fpf-single(x; v), fpf-dom(eq; x; f), fpf-ap(f; eq; x), ff, bor(p; q), eqof(d), b, P  Q, False, P  Q, P  Q, P  Q, fpf-compatible(A; a.B(a); eq; f; g), P  Q, prop{i:l}, x(s), EqDecider(T), x:A. B(x), t  T
Lemmas	deq wf, deq property, assert of bor, bor wf, assert wf, bfalse wf, eqof wf, subtype rel self